(DEFPROP PLNRFNS
 (PLNRFNS (DECLARE (DF *FEXPR (X) (MAPC (FUNCTION (LAMBDA (X) (PUTPROP X T (QUOTE *FSUBR)))) X))
		   (*FEXPR THAPPLY THGENAME THSTATE THANTE THERASING THCONSE THDUMP THRESTRICT THBKPT THUNIQUE)
		   (*FEXPR THVSETQ THMESSAGE THDO THGOAL THERASE THAND THNV THSUCCEED THAMONG THCOND THSETQ)
		   (*FEXPR THASSERT THASVAL THERT THGO THFAIL THOR THFIND THFINALIZE THRETURN THPROG THFLUSH)
		   (*FEXPR THNOT THV THTRACE THGENS)
		   (DEFPROP THBRANCH T *SUBR)
		   (DEFPROP THSPRINT T *SUBR)
		   (DEFPROP THMATCH T *LSUBR)
		   (SPECIAL THLAS OBLIST THINF THGENAME THGENS THZ THY THX THALIST THABRANCH THBRANCH)
		   (SPECIAL THV /0RETVAL /0LISTEN THL /0RETFLAG THE /0LEVEL THXX THTT TYPE THWH THON THML)
		   (SPECIAL THBS THNF THPC XX THAL THZ1 THY1 ↑A THTTL THA2 LASTWORD THFSTP THFST)
		   (SPECIAL THUSERCHARS THEXP THTREE THLEVEL THTRACE THPRD THMESSAGE THUSERMESSAGES)
		   (SPECIAL THUNREADFLG THUNREAD1 THUNREAD2 GRINPROPS THOLIST THVALUE THUSERINITFN)
		   (DE THCMPDEF
		       (X)
		       (COND ((ATOM (CADDR X)) (FLUSHEXPR X))
			     (T (COMPFUNC (CADR X) (CONS (QUOTE SUBR) (CDADDR X)) (CADDDR X)))))
		   (MAPC (FUNCTION (LAMBDA (X) (PUTPROP X (QUOTE THCMPDEF) (QUOTE DEFACTION))))
			 (QUOTE (THFAIL THSUCCEED THTRACE))))
	  THPUSH
	  EVLIS
	  THPRINT2
	  THPRINTC
	  THADD
	  THAMONG
	  THAMONGF
	  THAND
	  THANDF
	  THANDT
	  THANTE
	  THAPPLY
	  THAPPLY1
	  THASS1
	  THASSERT
	  THASSERTF
	  THASSERTT
	  THASVAL
	  THBA
	  THBAP
	  THBIND
	  THBI1
	  THBKPT
	  THBRANCH
	  THBRANCHUN
	  THCOND
	  THCONDF
	  THCONDT
	  THCONSE
	  THDATA
	  THDEF
	  THDO
	  THDO1
	  THDOB
	  THDUMP
	  THERASE
	  THERASEF
	  THERASET
	  THERASING
	  THFAIL
	  THFAIL?
	  THFAIL?F
	  THFAIL?T
	  THFINALIZE
	  THFIND
	  THFINDF
	  THFINDT
	  THFLUSH
	  THGAL
	  THGENAME
	  THGO
	  THGOAL
	  THGOALF
	  THGOALT
	  THIP
	  THMATCH2
	  THCHECK
	  THUNION
	  THMATCH
	  THMATCH1
	  THMATCHLIST
	  THMESSAGE
	  THMESSAGEF
	  THMESSAGET
	  THMUNGF
	  THMUNGT
	  THNOFAIL
	  THNOHASH
	  THNOT
	  THNV
	  THOR
	  THOR2
	  THORF
	  THORT
	  THPOPT
	  THPROG
	  THPROGA
	  THPROGF
	  THPROGT
	  THPURE
	  THPUTPROP
	  THREM1
	  THREMBINDF
	  THREMBINDT
	  THREMOVE
	  THREMPROP
	  THRESTRICT
	  THRETURN
	  THRPLACA
	  THRPLACAS
	  THURPLACA
	  THRPLACD
	  THRPLACDS
	  THURPLACD
	  THSETQ
	  THSGAL
	  THSTATE
	  THSUCCEED
	  THTAE
	  THTAG
	  THTAGF
	  THTAGT
	  THTRUE
	  THTRY1
	  THTRY
	  THUNDOF
	  THUNDOT
	  THUNIQUE
	  THUCI
	  THV1
	  THV
	  THVAL
	  THVAR
	  THVARS2
	  THVARSUBST
	  THVSETQ
	  THMUNG
	  THUNDO
	  THREMBIND
	  (PUTPROP (QUOTE THSPRINT) (GET (QUOTE SPRINT) (QUOTE SUBR)) (QUOTE SUBR))
	  SPRINT
	  THUNREADM
	  THREAD
	  THUSERCHARS
	  THERT
	  THEDIT
	  THINIT
	  THTRACE
	  THTRACE1
	  THUNTRACE
	  THTRACES
	  THSEL
	  THGENS
	  THEOREM
	  THUNREADFLG
	  THUNREAD1
	  THUNREAD2
	  GRINPROPS
	  THUSERINITFN
	  ↑A
	  THXX
	  THALIST
	  THUSERMESSAGES
	  PLNRINITFN
	  (PROGN
	   (DEFPROP PINIT
		    (LAMBDA NIL
		     (PROG (X)
			   (RPLACD (MEMQ# (QUOTE THEOREM) GRINPROPS) NIL)
			   (MODCHR (CHRVAL (QUOTE ')) (MODCHR (CHRVAL (QUOTE /@)) NIL))
			   (DRM $ THREAD)
			   (DRM : THREAD)
			   (INITFN (QUOTE THINIT))
			   (EXCISE)
			   (SETQ KLIST NIL)
			   (PUTPROP (QUOTE INITFN)
				    (CADR (SETQ X (GETL (QUOTE PLNRINITFN) (QUOTE (EXPR SUBR)))))
				    (CAR X))
			   (SETQ THUNREADFLG T)
			   (REMOB PLNRFNS PINIT PLNRINITFN)))
		    EXPR)))
VALUE)

(DECLARE (DF *FEXPR (X) (MAPC (FUNCTION (LAMBDA (X) (PUTPROP X T (QUOTE *FSUBR)))) X))
	 (*FEXPR THAPPLY THGENAME THSTATE THANTE THERASING THCONSE THDUMP THRESTRICT THBKPT THUNIQUE)
	 (*FEXPR THVSETQ THMESSAGE THDO THGOAL THERASE THAND THNV THSUCCEED THAMONG THCOND THSETQ)
	 (*FEXPR THASSERT THASVAL THERT THGO THFAIL THOR THFIND THFINALIZE THRETURN THPROG THFLUSH)
	 (*FEXPR THNOT THV THTRACE THGENS)
	 (DEFPROP THBRANCH T *SUBR)
	 (DEFPROP THSPRINT T *SUBR)
	 (DEFPROP THMATCH T *LSUBR)
	 (SPECIAL THLAS OBLIST THINF THGENAME THGENS THZ THY THX THALIST THABRANCH THBRANCH)
	 (SPECIAL THV /0RETVAL /0LISTEN THL /0RETFLAG THE /0LEVEL THXX THTT TYPE THWH THON THML)
	 (SPECIAL THBS THNF THPC XX THAL THZ1 THY1 ↑A THTTL THA2 LASTWORD THFSTP THFST)
	 (SPECIAL THUSERCHARS THEXP THTREE THLEVEL THTRACE THPRD THMESSAGE THUSERMESSAGES)
	 (SPECIAL THUNREADFLG THUNREAD1 THUNREAD2 GRINPROPS THOLIST THVALUE THUSERINITFN)
	 (DE THCMPDEF
	     (X)
	     (COND ((ATOM (CADDR X)) (FLUSHEXPR X))
		   (T (COMPFUNC (CADR X) (CONS (QUOTE SUBR) (CDADDR X)) (CADDDR X)))))
	 (MAPC (FUNCTION (LAMBDA (X) (PUTPROP X (QUOTE THCMPDEF) (QUOTE DEFACTION))))
	       (QUOTE (THFAIL THSUCCEED THTRACE))))

(DEFPROP THPUSH
 (LAMBDA (A) (LIST (QUOTE SETQ) (CADR A) (LIST (QUOTE CONS) (CADDR A) (CADR A))))
MACRO)

(DEFPROP EVLIS
 (LAMBDA (X) (MAPC (FUNCTION EVAL) X))
EXPR)

(DEFPROP THPRINT2
 (LAMBDA (X) (PRINC (QUOTE / )) (PRINC X))
EXPR)

(DEFPROP THPRINTC
 (LAMBDA (X) (TERPRI) (PRINC X) (PRINC (QUOTE / )))
EXPR)

(DEFPROP THADD
 (LAMBDA(THTT THPL)
  (PROG	(THNF THWH THCK THLAS THTTL THT1 THFST THFSTP THFOO)
	(SETQ THCK
	      (COND ((ATOM THTT)
		     (OR# (SETQ THT1 (GET THTT (QUOTE THEOREM)))
			  (PROG2 (PRINT THTT) (THERT CANT THASSERT/, NO THEOREM - THADD)))
		     (SETQ THWH (CAR THT1))
		     (SETQ THTTL THTT)
		     (AND# THPL
			   (PROG NIL
			    LP	 (THPUTPROP THTT (CADR THPL) (CAR THPL))
				 (COND ((SETQ THPL (CDDR THPL)) (GO LP)))))
		     (CADDR THT1))
		    (T (SETQ THWH (QUOTE THASSERTION)) (SETQ THTTL (CONS THTT THPL)) THTT)))
	(SETQ THNF 0)
	(SETQ THLAS (LENGTH THCK))
	(SETQ THFST T)
   THP1	(COND ((NULL THCK) (SETQ THCK THFOO)
			   (SETQ THNF 0)
			   (SETQ THFOO (SETQ THFST NIL))
			   (SETQ THFSTP T)
			   (GO THP1))
	      ((NULL (SETQ THT1 (THIP (CAR THCK)))) (RETURN NIL))
	      ((EQ THT1 (QUOTE THOK)))
	      ((SETQ THFOO (NCONC THFOO (LIST (COND ((EQ THT1 (QUOTE THVRB)) (CAR THCK))))))
	       (SETQ THCK (CDR THCK))
	       (GO THP1)))
	(SETQ THFST NIL)
	(MAPC (FUNCTION THIP) (CDR THCK))
	(SETQ THNF 0)
	(MAPC (FUNCTION THIP) THFOO)
	(RETURN THTTL)))
EXPR)

(DEFPROP THAMONG
 (LAMBDA(THA)
  (COND	((EQ (CADR
	      (SETQ THXX
		    (THGAL (COND ((EQ (CAAR THA) (QUOTE THEV)) (THVAL (CADAR THA) THALIST)) (T (CAR THA)))
			   THALIST)))
	     (QUOTE THUNASSIGNED))
	 (THPUSH THTREE (LIST (QUOTE THAMONG) THXX (THVAL (CADR THA) THALIST)))
	 NIL)
	(T (MEMBER# (CADR THXX) (THVAL (CADR THA) THALIST)))))
FEXPR)

(DEFPROP THAMONG
 THAMONGF
THFAIL)

(DEFPROP THAMONGF
 (LAMBDA NIL
  (COND	(THMESSAGE (THPOPT) NIL)
	((CADDAR THTREE) (RPLACA (CDADAR THTREE) (CAADDR (CAR THTREE)))
			 (RPLACA (CDDAR THTREE) (CDADDR (CAR THTREE)))
			 (SETQ THBRANCH THTREE)
			 (SETQ THABRANCH THALIST)
			 (THPOPT)
			 T)
	(T (RPLACA (CDADAR THTREE) (QUOTE THUNASSIGNED)) (THPOPT) NIL)))
EXPR)

(DEFPROP THAND
 (LAMBDA (A) (OR# (NOT A) (PROG2 (THPUSH THTREE (LIST (QUOTE THAND) A NIL)) (SETQ THEXP (CAR A)))))
FEXPR)

(DEFPROP THAND
 THANDT
THSUCCEED)

(DEFPROP THAND
 THANDF
THFAIL)

(DEFPROP THANDF
 (LAMBDA NIL (THBRANCHUN) NIL)
EXPR)

(DEFPROP THANDT
 (LAMBDA NIL
  (COND	((CDADAR THTREE) (THBRANCH) (SETQ THEXP (CADR (CADAR THTREE))) (RPLACA (CDAR THTREE) (CDADAR THTREE)))
	((THPOPT)))
  THVALUE)
EXPR)

(DEFPROP THANTE
 (LAMBDA (THX) (THDEF (QUOTE THANTE) THX))
FEXPR)

(DEFPROP THAPPLY
 (LAMBDA (L) (THAPPLY1 (CAR L) (GET (CAR L) (QUOTE THEOREM)) (CADR L)))
FEXPR)

(DEFPROP THAPPLY1
 (LAMBDA(THM THB DAT)
  (COND	((AND# (THBIND (CADR THB)) (THMATCH1 DAT (CADDR THB)))
	 (AND# THTRACE (THTRACES (QUOTE THEOREM) THM))
	 (THPUSH THTREE (LIST (QUOTE THPROG) (CDDR THB) NIL (CDDR THB)))
	 (THPROGA)
	 T)
	(T (SETQ THALIST THOLIST) (THPOPT) NIL)))
EXPR)

(DEFPROP THASS1
 (LAMBDA(THA P)
  (PROG	(THX THY1 THY TYPE PSEUDO)
	(AND# (CDR THA) (EQ (CAADR THA) (QUOTE THPSEUDO)) (SETQ PSEUDO T))
	(OR# (ATOM (SETQ THX (CAR THA)))
	     (THPURE (SETQ THX (THVARSUBST THX NIL)))
	     PSEUDO
	     (PROG2 (PRINT THX) (THERT IMPURE ASSERTION OR ERASURE - THASS1)))
	(AND THTRACE (NOT PSEUDO) (THTRACES (COND (P (QUOTE THASSERT)) ((QUOTE THERASE))) THX))
	(SETQ THA (COND (PSEUDO (CDDR THA)) ((CDR THA))))
	(COND ((SETQ THX
		     (COND (PSEUDO (LIST THX))
			   (P
			    (THADD THX
				   (SETQ THY
					 (COND
					  ((AND# THA (EQ (CAAR THA) (QUOTE THPROP)))
					   (PROG1 (EVAL (CADAR THA)) (SETQ THA (CDR THA))))))))
			   (T (THREMOVE THX)))))
	      (T (RETURN NIL)))
	(COND (P (SETQ TYPE (QUOTE THANTE))) ((SETQ TYPE (QUOTE THERASING))))
	(OR# PSEUDO (THPUSH THTREE (LIST (COND (P (QUOTE THASSERT)) ((QUOTE THERASE))) THX THY)))
	(SETQ THY (MAPCAN (FUNCTION THTAE) THA))
	(COND (THY (SETQ THEXP (CONS (QUOTE THDO) THY))))
	(RETURN THX)))
EXPR)

(DEFPROP THASSERT
 (LAMBDA (THA) (THASS1 THA T))
FEXPR)

(DEFPROP THASSERT
 THASSERTT
THSUCCEED)

(DEFPROP THASSERT
 THASSERTF
THFAIL)

(DEFPROP THASSERT
 (LAMBDA(X B)
  (THPUSH THTREE (LIST (QUOTE THTRACES) (THGENS A) (AND# B (QUOTE (THERT)))))
  (PRINT (QUOTE ASSERTING))
  (PRIN1 (CADAR THTREE))
  (PRINC (QUOTE / ))
  (PRIN1 X))
THTRACE)

(DEFPROP THASSERTF
 (LAMBDA NIL (THREMOVE (COND ((ATOM (CADAR THTREE)) (CADAR THTREE)) (T (CAADAR THTREE)))) (THPOPT) NIL)
EXPR)

(DEFPROP THASSERTT
 (LAMBDA NIL (PROG1 (CADAR THTREE) (THPOPT)))
EXPR)

(DEFPROP THASVAL
 (LAMBDA (X) ((LAMBDA (X) (AND# X (NOT (EQ (CADR X) (QUOTE THUNASSIGNED))))) (THGAL (CAR X) THALIST)))
FEXPR)

(DEFPROP THBA
 (LAMBDA(TH1 TH2)
  (PROG	(THP)
	(SETQ THP TH2)
   THP1	(AND# (EQ (COND (THPC (CADR THP)) (T (CAADR THP))) TH1) (RETURN THP))
	(COND ((CDR (SETQ THP (CDR THP)))) (T (RETURN NIL)))
	(GO THP1)))
EXPR)

(DEFPROP THBAP
 (LAMBDA(TH1 TH2)
  (PROG	(THP)
	(SETQ THP TH2)
   THP1	(AND# (EQUAL (COND (THPC (CADR THP)) (T (CAADR THP))) TH1) (RETURN THP))
	(COND ((CDR (SETQ THP (CDR THP)))) (T (RETURN NIL)))
	(GO THP1)))
EXPR)

(DEFPROP THBIND
 (LAMBDA(A)
  (SETQ THOLIST THALIST)
  (OR# (NULL A)
       (PROG NIL
	GO   (COND ((NULL A) (THPUSH THTREE (LIST (QUOTE THREMBIND) THOLIST)) (RETURN T)))
	     (THPUSH THALIST
		     (COND ((ATOM (CAR A)) (LIST (CAR A) (QUOTE THUNASSIGNED)))
			   ((EQ (CAAR A) (QUOTE THRESTRICT)) (NCONC (THBI1 (CADAR A)) (CDDAR A)))
			   (T (LIST (CAAR A) (EVAL (CADAR A))))))
	     (SETQ A (CDR A))
	     (GO GO))))
EXPR)

(DEFPROP THBI1
 (LAMBDA (X) (COND ((ATOM X) (LIST X (QUOTE THUNASSIGNED))) (T (LIST (CAR X) (EVAL (CADR X))))))
EXPR)

(DEFPROP THBKPT
 (LAMBDA (L) (OR# (AND# THTRACE (THTRACES (QUOTE THBKPT) L)) THVALUE))
FEXPR)

(DEFPROP THBKPT
 (LAMBDA(X B)
  (THPUSH THTREE (LIST (QUOTE THTRACES) (THGENS B) (AND# B (QUOTE (THERT)))))
  (THPRINTC (QUOTE PASSING/ BKPT))
  (PRIN1 (CADAR THTREE))
  (PRINC (QUOTE / ))
  (SETQ THBRANCH THTREE)
  (SETQ THABRANCH THALIST)
  (THPOPT)
  (PRIN1 X))
THTRACE)

(DEFPROP THBRANCH
 (LAMBDA NIL
  (COND	((NOT (CDADAR THTREE)))
	((EQ THBRANCH THTREE) (SETQ THBRANCH NIL))
	((RPLACA (CDDAR THTREE) (CONS (LIST THBRANCH THABRANCH (CADAR THTREE)) (CADDAR THTREE)))
	 (SETQ THBRANCH NIL))))
EXPR)

(DEFPROP THBRANCHUN
 (LAMBDA NIL
  (PROG	(X)
	(RETURN
	 (COND ((SETQ X (CADDAR THTREE))
		(RPLACA (CDAR THTREE) (CADDAR X))
		(RPLACA (CDDAR THTREE) (CDR X))
		(SETQ THALIST (CADAR X))
		(SETQ THTREE (CAAR X))
		T)
	       (T (THPOPT) NIL)))))
EXPR)

(DEFPROP THCOND
 (LAMBDA (THA) (THPUSH THTREE (LIST (QUOTE THCOND) THA NIL)) (SETQ THEXP (CAAR THA)))
FEXPR)

(DEFPROP THCOND
 THCONDT
THSUCCEED)

(DEFPROP THCOND
 THCONDF
THFAIL)

(DEFPROP THCONDF
 (LAMBDA NIL (THOR2 NIL))
EXPR)

(DEFPROP THCONDT
 (LAMBDA NIL (RPLACA (CAR THTREE) (QUOTE THAND)) (RPLACA (CDAR THTREE) (CAADAR THTREE)) THVALUE)
EXPR)

(DEFPROP THCONSE
 (LAMBDA (THX) (THDEF (QUOTE THCONSE) THX))
FEXPR)

(DEFPROP THDATA
 (LAMBDA NIL
  (PROG (X) GO (TERPRI) (COND ((NULL (SETQ X (READ))) (RETURN T)) ((PRINT (THADD (CAR X) (CDR X))))) (GO GO)))
EXPR)

(DEFPROP THDEF
 (LAMBDA(THMTYPE THX)
  (PROG	(THNOASSERT? THMNAME THMBODY)
	(COND ((NOT (ATOM (CAR THX)))
	       (SETQ THMBODY THX)
	       (COND ((EQ THMTYPE (QUOTE THCONSE)) (SETQ THMNAME (THGENAME TC-G)))
		     ((EQ THMTYPE (QUOTE THANTE)) (SETQ THMNAME (THGENAME TA-G)))
		     ((EQ THMTYPE (QUOTE THERASING)) (SETQ THMNAME (THGENAME TE-G)))))
	      ((SETQ THMNAME (CAR THX)) (SETQ THMBODY (CDR THX))))
	(COND ((EQ (CAR THMBODY) (QUOTE THNOASSERT)) (SETQ THNOASSERT? T) (SETQ THMBODY (CDR THMBODY))))
	(THPUTPROP THMNAME (CONS THMTYPE THMBODY) (QUOTE THEOREM))
	(COND (THNOASSERT? (PRINT (LIST THMNAME (QUOTE DEFINED) (QUOTE BUT) (QUOTE NOT) (QUOTE ASSERTED))))
	      ((THASS1 (LIST THMNAME) T) (PRINT (LIST THMNAME (QUOTE DEFINED) (QUOTE AND) (QUOTE ASSERTED))))
	      (T (PRINT (LIST THMNAME (QUOTE REDEFINED)))))
	(RETURN T)))
EXPR)

(DEFPROP THDO
 (LAMBDA (A) (OR# (NOT A) (PROG2 (THPUSH THTREE (LIST (QUOTE THDO) A NIL NIL)) (SETQ THEXP (CAR A)))))
FEXPR)

(DEFPROP THDO
 THDOB
THSUCCEED)

(DEFPROP THDO
 THDOB
THFAIL)

(DEFPROP THDO1
 (LAMBDA NIL
  (RPLACA (CDAR THTREE) (CDADAR THTREE))
  (SETQ THEXP (CAADAR THTREE))
  (COND
   (THBRANCH (RPLACA (CDDAR THTREE) (CONS THBRANCH (CADDAR THTREE)))
	     (SETQ THBRANCH NIL)
	     (RPLACA (CDDDAR THTREE) (CONS THABRANCH (CAR (CDDDAR THTREE)))))))
EXPR)

(DEFPROP THDOB
 (LAMBDA NIL (COND ((OR# THMESSAGE (NULL (CDADAR THTREE))) (RPLACA (CAR THTREE) (QUOTE THUNDO)) T) ((THDO1))))
EXPR)

(DEFPROP THDUMP
 (LAMBDA(THFILE)
  (OUTC	(PROG1 (OUTC (EVAL (LIST (QUOTE OUTPUT) (QUOTE DSK:) (CAR THFILE))) NIL)
	       (EVAL (CONS (QUOTE THSTATE) (CDR THFILE))))
	T))
FEXPR)

(DEFPROP THERASE
 (LAMBDA (THA) (THASS1 THA NIL))
FEXPR)

(DEFPROP THERASE
 THERASET
THSUCCEED)

(DEFPROP THERASE
 THERASEF
THFAIL)

(DEFPROP THERASE
 (LAMBDA(X B)
  (THPUSH THTREE (LIST (QUOTE THTRACES) (THGENS E) (AND# B (QUOTE (THERT)))))
  (PRINT (QUOTE ERASING))
  (PRIN1 (CADAR THTREE))
  (PRINC (QUOTE / ))
  (PRIN1 X))
THTRACE)

(DEFPROP THERASEF
 (LAMBDA NIL
  (THADD (COND ((ATOM (CADAR THTREE)) (CADAR THTREE)) (T (CAADAR THTREE)))
	 (COND ((ATOM (CADAR THTREE)) NIL) (T (CDADAR THTREE))))
  (THPOPT)
  NIL)
EXPR)

(DEFPROP THERASET
 (LAMBDA NIL (PROG1 (CADAR THTREE) (THPOPT)))
EXPR)

(DEFPROP THERASING
 (LAMBDA (THX) (THDEF (QUOTE THERASING) THX))
FEXPR)

(DEFPROP THFAIL
 (LAMBDA(THA)
  (AND#	THA
	(PROG (THTREE1 THA1 THX)
	 F    (COND ((EQ (CAR THA) (QUOTE THEOREM)) (SETQ THA1 (QUOTE THPROG)))
		    ((EQ (CAR THA) (QUOTE THTAG)) (SETQ THA1 (QUOTE THPROG)))
		    ((EQ (CAR THA) (QUOTE THINF)) (SETQ THINF T) (RETURN NIL))
		    ((EQ (CAR THA) (QUOTE THMESSAGE)) (SETQ THMESSAGE (CADR THA)) (RETURN NIL))
		    (T (SETQ THA1 (CAR THA))))
	      (SETQ THTREE1 THTREE)
	 LP1  (COND ((NULL THTREE1)
		     (PRINT THA)
		     (COND ((ATOM (SETQ THA (THERT NOT FOUND - THFAIL))) (RETURN THA)) (T (GO F))))
		    ((EQ (CAAR THTREE1) THA1) (GO ELP1)))
	 ALP1 (SETQ THTREE1 (CDR THTREE1))
	      (GO LP1)
	 ELP1 (COND
	       ((EQ (CAR THA) (QUOTE THTAG))
		(COND ((MEMQ# (CADR THA) (CADDDR (CAR THTREE1))) (GO TAGS)) (T (GO ALP1)))))
	      (SETQ THMESSAGE (LIST (CDR THTREE1) (AND# (CDR THA) (CADR THA))))
	      (RETURN NIL)
	 TAGS (SETQ THX (CADDAR THTREE1))
	 LP2  (COND ((NULL THX) (GO ALP1))
		    ((EQ (CAADDR (CAR THX)) (CADR THA))
		     (SETQ THMESSAGE (LIST (CAAR THX) (AND# (CDDR THA) (CADDR THA))))
		     (RETURN NIL)))
	      (SETQ THX (CDR THX))
	      (GO LP2))))
FEXPR)

(DEFPROP THFAIL?
 (LAMBDA (PRD ACT) (THPUSH THTREE (LIST (QUOTE THFAIL?) PRD ACT)) THVALUE)
EXPR)

(DEFPROP THFAIL?
 THFAIL?T
THSUCCEED)

(DEFPROP THFAIL?
 THFAIL?F
THFAIL)

(DEFPROP THFAIL?F
 (LAMBDA NIL
  (COND ((EVAL (CADAR THTREE)) (PROG2 (SETQ THMESSAGE NIL) (EVAL (CADDAR THTREE)) (THPOPT))) (T (THPOPT) NIL)))
EXPR)

(DEFPROP THFAIL?T
 (LAMBDA NIL (THPOPT) THVALUE)
EXPR)

(DEFPROP THFINALIZE
 (LAMBDA(THA)
  (PROG	(THTREE1 THT THX)
	(COND ((NULL THA) (SETQ THA (THERT BAD CALL - THFINALIZE))))
	(COND ((ATOM THA) (RETURN THA))
	      ((EQ (CAR THA) (QUOTE THTAG)) (SETQ THT (CADR THA)))
	      ((EQ (CAR THA) (QUOTE THEOREM)) (SETQ THA (LIST (QUOTE THPROG)))))
	(SETQ THTREE (SETQ THTREE1 (CONS NIL THTREE)))
   PLUP	(SETQ THX (CADR THTREE1))
	(COND ((NULL (CDR THTREE1)) (PRINT THA) (THERT OVERPOP - THFINALIZE))
	      ((AND# THT (EQ (CAR THX) (QUOTE THPROG)) (MEMQ# THT (CADDDR THX))) (GO RTLEV))
	      ((OR# (EQ (CAR THX) (QUOTE THPROG)) (EQ (CAR THX) (QUOTE THAND)))
	       (RPLACA (CDDR THX) NIL)
	       (SETQ THTREE1 (CDR THTREE1)))
	      ((EQ (CAR THX) (QUOTE THREMBIND)) (SETQ THTREE1 (CDR THTREE1)))
	      ((RPLACD THTREE1 (CDDR THTREE1))))
	(COND ((EQ (CAR THX) (CAR THA)) (GO DONE)))
	(GO PLUP)
   RTLEV
	(SETQ THX (CDDR THX))
   LEVLP
	(COND ((NULL (CAR THX)) (SETQ THTREE1 (CDR THTREE1)) (GO PLUP))
	      ((EQ (CAADDR (CAAR THX)) THT) (GO DONE)))
	(RPLACA THX (CDAR THX))
	(GO LEVLP)
   DONE	(SETQ THTREE (CDR THTREE))
	(RETURN T)))
FEXPR)

(DEFPROP THFIND
 (LAMBDA(THA)
  (THBIND (CADDR THA))
  (THPUSH THTREE
	  (LIST	(QUOTE THFIND)
		(COND ((EQ (CAR THA) (QUOTE ALL)) (QUOTE (1 NIL NIL)))
		      ((NUMBERP (CAR THA)) (LIST (CAR THA) (CAR THA) T))
		      ((NUMBERP (CAAR THA)) (CAR THA))
		      ((EQ (CAAR THA) (QUOTE EXACTLY)) (LIST (CADAR THA) (ADD1 (CADAR THA)) NIL))
		      ((EQ (CAAR THA) (QUOTE AT-MOST)) (LIST 1 (ADD1 (CADAR THA)) NIL))
		      ((EQ (CAAR THA) (QUOTE AS-MANY-AS)) (LIST 1 (CADAR THA) T))
		      (T
		       (CONS (CADAR THA)
			     (COND ((NULL (CDDAR THA)) (LIST NIL T))
				   ((EQ (CADDAR THA) (QUOTE AT-MOST)) (LIST (ADD1 (CAR (CDDDAR THA))) NIL))
				   (T (LIST (CAR (CDDDAR THA)) T))))))
		(CONS 0 NIL)
		(CADR THA)))
  (THPUSH THTREE (LIST (QUOTE THPROG) (CDDR THA) NIL (CDDR THA)))
  (THPROGA))
FEXPR)

(DEFPROP THFIND
 THFINDT
THSUCCEED)

(DEFPROP THFIND
 THFINDF
THFAIL)

(DEFPROP THFINDF
 (LAMBDA NIL
  (SETQ THBRANCH NIL)
  (COND	((OR# THMESSAGE (LESSP (CAADR (SETQ THXX (CDAR THTREE))) (CAAR THXX))) (THPOPT) NIL)
	(T (THPOPT) (CDADR THXX))))
EXPR)

(DEFPROP THFINDT
 (LAMBDA NIL
  (PROG	(THX THY THZ THCDAR)
	(SETQ THZ (CADDR (SETQ THCDAR (CDAR THTREE))))
	(AND# (MEMBER# (SETQ THX (THVARSUBST THZ NIL)) (CDADR THCDAR)) (GO GO))
	(RPLACD (CADR THCDAR) (CONS THX (CDADR THCDAR)))
	(COND
	 ((EQ (SETQ THY (ADD1 (CAADR THCDAR))) (CADAR THCDAR))
	  (RETURN (PROG2 (SETQ THBRANCH NIL) (AND# (CADDAR THCDAR) (CDADR THCDAR)) (THPOPT)))))
	(RPLACA (CADR THCDAR) THY)
   GO	(SETQ THTREE THBRANCH)
	(SETQ THALIST THABRANCH)
	(SETQ THBRANCH NIL)
	(RETURN NIL)))
EXPR)

(DEFPROP THFLUSH
 (LAMBDA(A)
  (MAPC	(FUNCTION
	 (LAMBDA (B) (MAPC (FUNCTION (LAMBDA (C) (MAPC (FUNCTION (LAMBDA (D) (REMPROP D B))) C))) OBLIST)))
	(SETQ A (OR# A (QUOTE (THASSERTION THCONSE THANTE THERASING)))))
  A)
FEXPR)

(DEFPROP THGAL
 (LAMBDA (X Y) (SETQ THXX X) (OR# (ASSOC (CADR X) Y) (PROG2 (PRINT THXX) (THERT THUNBOUND THGAL))))
EXPR)

(DEFPROP THGENAME
 (LAMBDA (X) (READLIST (NCONC (EXPLODE (CAR X)) (EXPLODE (SETQ THGENAME (ADD1 THGENAME))))))
FEXPR)

(DEFPROP THGENAME
 (THGENAME . 0)
VALUE)

(DEFPROP THGO
 (LAMBDA (X) (APPLY# (QUOTE THSUCCEED) (CONS (QUOTE THTAG) X)))
FEXPR)

(DEFPROP THGOAL
 (LAMBDA(THA)
  (PROG	(THY THY1 THZ THZ1 THA1 THA2)
	(SETQ THA2 (THVARSUBST (CAR THA) T))
	(SETQ THA1 (CDR THA))
	(COND
	 ((OR# (NULL THA1)
	       (AND# (NOT
		      (AND# (EQ (CAAR THA1) (QUOTE THANUM))
			    (SETQ THA1
				  (CONS	(LIST (QUOTE THNUM) (CADAR THA1))
					(CONS (LIST (QUOTE THDBF) (QUOTE THTRUE)) (CDR THA1))))))
		     (NOT (AND# (EQ (CAAR THA1) (QUOTE THNODB)) (PROG2 (SETQ THA1 (CDR THA1)) T)))
		     (NOT (EQ (CAAR THA1) (QUOTE THDBF)))))
	  (SETQ THA1 (CONS (LIST (QUOTE THDBF) (QUOTE THTRUE)) THA1))))
	(SETQ THA1 (MAPCAN (FUNCTION THTRY) THA1))
	(AND# THTRACE (THTRACES (QUOTE THGOAL) THA2))
	(COND ((NULL THA1) (RETURN NIL)))
	(THPUSH THTREE (LIST (QUOTE THGOAL) THA2 THA1))
	(RPLACD (CDDAR THTREE) 777777)
	(RETURN NIL)))
FEXPR)

(DEFPROP THGOAL
 THGOALT
THSUCCEED)

(DEFPROP THGOAL
 THGOALF
THFAIL)

(DEFPROP THGOAL
 (LAMBDA(X B)
  (THPUSH THTREE
	  (LIST (QUOTE THTRACES) (THGENS G) (QUOTE (AND# THVALUE (PRIN1 THVALUE))) (AND# B (QUOTE (THERT)))))
  (THPRINTC (QUOTE TRYING/ GOAL))
  (PRIN1 (CADAR THTREE))
  (PRINC (QUOTE / ))
  (PRIN1 X))
THTRACE)

(DEFPROP THGOALF
 (LAMBDA NIL (COND (THMESSAGE (THPOPT) NIL) ((THTRY1)) (T (THPOPT) NIL)))
EXPR)

(DEFPROP THGOALT
 (LAMBDA NIL (PROG1 (COND ((EQ THVALUE (QUOTE THNOVAL)) (THVARSUBST (CADAR THTREE) NIL)) (THVALUE)) (THPOPT)))
EXPR)

(DEFPROP THIP
 (LAMBDA(THI)
  (PROG	(THT1 THT3 THSV THT2 THI1)
	(SETQ THNF (ADD1 THNF))
	(COND ((AND# (ATOM THI) (NOT (EQ THI (QUOTE ?))) (NOT (NUMBERP THI))) (SETQ THI1 THI))
	      ((OR# (EQ THI (QUOTE ?)) (MEMQ# (CAR THI) (QUOTE (THV THNV))))
	       (COND (THFST (RETURN (QUOTE THVRB))) ((SETQ THI1 (QUOTE THVRB)))))
	      (T (RETURN (QUOTE THVRB))))
	(COND ((NOT (SETQ THT1 (GET THI1 THWH)))
	       (PUTPROP THI1 (LIST NIL (LIST THNF (LIST THLAS 1 THTTL))) THWH))
	      ((EQ THT1 (QUOTE THNOHASH)) (RETURN (QUOTE THBQF)))
	      ((NOT (SETQ THT2 (ASSOC THNF (CDR THT1)))) (NCONC THT1 (LIST (LIST THNF (LIST THLAS 1 THTTL)))))
	      ((NOT (SETQ THT3 (ASSOC THLAS (CDR THT2)))) (NCONC THT2 (LIST (LIST THLAS 1 THTTL))))
	      ((AND# (OR# THFST THFSTP)
		     (COND ((EQ THWH (QUOTE THASSERTION)) (ASSOC# THTT (CDDR THT3)))
			   (T (MEMQ# THTT (CDDR THT3)))))
	       (RETURN NIL))
	      ((SETQ THSV (CDDR THT3))
	       (RPLACA (CDR THT3) (ADD1 (CADR THT3)))
	       (RPLACD (CDR THT3) (NCONC (LIST THTTL) THSV))))
	(RETURN (QUOTE THOK))))
EXPR)

(DEFPROP THMATCH2
 (LAMBDA(THX THY)
  (AND# (EQ (CAR THX) (QUOTE THEV)) (SETQ THX (THVAL (CADR THX) THOLIST)))
  (AND# (EQ (CAR THY) (QUOTE THEV)) (SETQ THY (THVAL (CADR THY) THALIST)))
  (COND	((EQ THX (QUOTE ?)))
	((EQ THY (QUOTE ?)))
	((OR# (MEMQ# (CAR THX) (QUOTE (THV THNV THRESTRICT))) (MEMQ# (CAR THY) (QUOTE (THV THNV THRESTRICT))))
	 ((LAMBDA(XPAIR YPAIR)
	   (COND ((AND#	XPAIR
			(OR# (EQ (CAR THX) (QUOTE THNV))
			     (AND# (EQ (CAR THX) (QUOTE THV)) (EQ (CADR XPAIR) (QUOTE THUNASSIGNED))))
			(THCHECK (CDDR XPAIR) (COND (YPAIR (CADR YPAIR)) (T THY))))
		  (COND	(YPAIR (THRPLACAS (CDR XPAIR) (CADR YPAIR))
			       (AND# (CDDR YPAIR) (THRPLACDS (CDR XPAIR) (THUNION (CDDR XPAIR) (CDDR YPAIR))))
			       (THRPLACDS YPAIR (CDR XPAIR)))
			(T (THRPLACAS (CDR XPAIR) THY))))
		 ((AND#	YPAIR
			(OR# (EQ (CAR THY) (QUOTE THNV))
			     (AND# (EQ (CAR THY) (QUOTE THV)) (EQ (CADR YPAIR) (QUOTE THUNASSIGNED))))
			(THCHECK (CDDR YPAIR) (COND (XPAIR (CADR XPAIR)) (T THX))))
		  (COND (XPAIR (THRPLACAS (CDR YPAIR) (CADR XPAIR))) (T (THRPLACAS (CDR YPAIR) THX))))
		 ((AND# XPAIR (EQUAL (CADR XPAIR) (COND (YPAIR (CADR YPAIR)) (T THY)))))
		 ((AND# YPAIR (EQUAL (CADR YPAIR) THX)))
		 (T (ERR NIL))))
	  (COND	((THVAR THX) (THGAL THX THOLIST))
		((EQ (CAR THX) (QUOTE THRESTRICT))
		 (COND ((EQ (CADR THX) (QUOTE ?))
			(PROG1 (CONS (QUOTE ?) (CONS (QUOTE THUNASSIGNED) (APPEND (CDDR THX) NIL)))
			       (SETQ THX (QUOTE (THNV ?)))))
		       (T
			((LAMBDA (U) (THRPLACDS (CDR U) (THUNION (CDDR U) (CDDR THX))) (SETQ THX (CADR THX)) U)
			 (THGAL (CADR THX) THOLIST))))))
	  (COND	((THVAR THY) (THGAL THY THALIST))
		((EQ (CAR THY) (QUOTE THRESTRICT))
		 (COND ((EQ (CADR THY) (QUOTE ?))
			(PROG1 (CONS (QUOTE ?) (CONS (QUOTE THUNASSIGNED) (APPEND (CDDR THY) NIL)))
			       (SETQ THY (QUOTE (THNV ?)))))
		       (T
			((LAMBDA (U) (THRPLACDS (CDR U) (THUNION (CDDR U) (CDDR THY))) (SETQ THY (CADR THY)) U)
			 (THGAL (CADR THY) THALIST))))))))
	((EQUAL THX THY))
	(T (ERR NIL))))
EXPR)

(DEFPROP THCHECK
 (LAMBDA(THPRD THX)
  (OR# (NULL THPRD)
       (EQ THX (QUOTE THUNASSIGNED))
       (ERRSET (MAPC (FUNCTION (LAMBDA (THY) (OR# (THY THX) (ERR NIL)))) THPRD))))
EXPR)

(DEFPROP THUNION
 (LAMBDA (L1 L2) (MAPC (FUNCTION (LAMBDA (THX) (COND ((MEMBER# THX L2)) (T (SETQ L2 (CONS THX L2)))))) L1) L2)
EXPR)

(DEFPROP THMATCH
 (LAMBDA THX
  ((LAMBDA (THOLIST THALIST) (THMATCH1 (ARG 1) (ARG 2)))
   (COND ((GREATERP THX 2) (ARG 3)) (T THALIST))
   (COND ((GREATERP THX 3) (ARG 4)) (T THALIST))))
EXPR)

(DEFPROP THMATCH1
 (LAMBDA(THX THY)
  (PROG	(THML)
	(COND ((AND# (EQ (LENGTH
			  (COND ((EQ (CAR THX) (QUOTE THEV)) (SETQ THX (THVAL (CADR THX) THOLIST))) (THX)))
			 (LENGTH THY))
		     (ERRSET (MAPC (FUNCTION THMATCH2) THX THY)))
	       (AND# THML (THPUSH THTREE (LIST (QUOTE THMUNG) THML)))
	       (RETURN T))
	      (T (EVLIS THML) (RETURN NIL)))))
EXPR)

(DEFPROP THMATCHLIST
 (LAMBDA(THTB THWH)
  (PROG	(THB1 THB2 THL THNF THAL THA1 THA2 THRN THL1 THL2 THRVC)
	(SETQ THL 377777777777)
	(SETQ THNF 0)
	(SETQ THAL (LENGTH THTB))
	(SETQ THB1 THTB)
   THP1	(COND (THB1) (T (RETURN (COND (THL2 (APPEND THL1 THL2)) (THL1)))))
	(SETQ THNF (ADD1 THNF))
	(SETQ THB2 (CAR THB1))
	(SETQ THB1 (CDR THB1))
   THP3	(COND ((OR# (NULL (ATOM THB2)) (NUMBERP THB2) (EQ THB2 (QUOTE ?))) (GO THP1))
	      ((NOT (SETQ THA1 (GET THB2 THWH))) (SETQ THA1 (QUOTE (0 0))))
	      ((EQ THA1 (QUOTE THNOHASH)) (GO THP1))
	      ((NOT (SETQ THA1 (ASSOC THNF (CDR THA1)))) (SETQ THA1 (QUOTE (0 0))))
	      ((NOT (SETQ THA1 (ASSOC THAL (CDR THA1)))) (SETQ THA1 (QUOTE (0 0)))))
	(SETQ THRN (CADR THA1))
	(SETQ THA1 (CDDR THA1))
	(AND# (EQ THWH (QUOTE THASSERTION)) (GO THP2))
	(COND ((NOT (SETQ THA2 (GET (QUOTE THVRB) THWH))) (SETQ THA2 (QUOTE (0 0))))
	      ((NOT (SETQ THA2 (ASSOC THNF (CDR THA2)))) (SETQ THA2 (QUOTE (0 0))))
	      ((NOT (SETQ THA2 (ASSOC THAL (CDR THA2)))) (SETQ THA2 (QUOTE (0 0)))))
	(SETQ THRVC (CADR THA2))
	(SETQ THA2 (CDDR THA2))
	(AND# (GREATERP (PLUS THRVC THRN) THL) (GO THP1))
	(SETQ THL (PLUS THRVC THRN))
	(SETQ THL1 THA1)
	(SETQ THL2 THA2)
	(GO THP1)
   THP2	(COND ((EQ THRN 0) (RETURN NIL)) ((GREATERP THL THRN) (SETQ THL1 THA1) (SETQ THL THRN)))
	(GO THP1)))
EXPR)

(DEFPROP THMESSAGE
 (LAMBDA (THA) (THPUSH THTREE (CONS (QUOTE THMESSAGE) THA)) THVALUE)
FEXPR)

(DEFPROP THMESSAGE
 THMESSAGET
THSUCCEED)

(DEFPROP THMESSAGE
 THMESSAGEF
THFAIL)

(DEFPROP THMESSAGEF
 (LAMBDA NIL
  (PROG	(BOD)
	(SETQ BOD (CAR THTREE))
	(THPOPT)
	(COND ((AND# (THBIND (CADR BOD)) (THMATCH1 (CADDR BOD) THMESSAGE))
	       (THPUSH THTREE (LIST (QUOTE THPROG) (CDDR BOD) NIL (CDDR BOD)))
	       (SETQ THMESSAGE NIL)
	       (RETURN (THPROGA)))
	      (T (SETQ THALIST THOLIST) (THPOPT)))
	(RETURN NIL)))
EXPR)

(DEFPROP THMESSAGET
 (LAMBDA NIL (THPOPT) THVALUE)
EXPR)

(DEFPROP THMUNGF
 (LAMBDA NIL (EVLIS (CADAR THTREE)) (THPOPT) NIL)
EXPR)

(DEFPROP THMUNGT
 (LAMBDA NIL (THPOPT) THVALUE)
EXPR)

(DEFPROP THNOFAIL
 (LAMBDA (THX) (COND (THX (DEFPROP THPROG THPROGT THFAIL)) (T (DEFPROP THPROG THPROGF THFAIL))))
EXPR)

(DEFPROP THNOHASH
 (LAMBDA(THA)
  (PROG	(T1)
	(MAPC (FUNCTION (LAMBDA (X) (PUTPROP (CAR THA) (QUOTE THNOHASH) X)))
	      (SETQ T1 (OR# (CDR THA) (QUOTE (THASSERTION THCONSE THANTE THERASING)))))
	(RETURN T1)))
FEXPR)

(DEFPROP THNOT
 (LAMBDA (THA) (SETQ THEXP (LIST (QUOTE THCOND) (LIST (CAR THA) (QUOTE (THFAIL THAND))) (QUOTE ((THSUCCEED))))))
FEXPR)

(DEFPROP THNV
 (LAMBDA (X) (THV1 (CAR X)))
FEXPR)

(DEFPROP THOR
 (LAMBDA (THA) (AND# THA (THPUSH THTREE (LIST (QUOTE THOR) THA)) (SETQ THEXP (CAR THA))))
FEXPR)

(DEFPROP THOR
 THORT
THSUCCEED)

(DEFPROP THOR
 THORF
THFAIL)

(DEFPROP THOR2
 (LAMBDA(P)
  (COND	(THMESSAGE (THPOPT) NIL)
	((AND# (CADAR THTREE) (CDADAR THTREE))
	 (RPLACA (CDAR THTREE) (CDADAR THTREE))
	 (SETQ THEXP (COND (P (PROG1 (CAADAR THTREE) (OR# (CADAR THTREE) (THPOPT)))) ((CAR (CAADAR THTREE))))))
	(T (THPOPT) NIL)))
EXPR)

(DEFPROP THORF
 (LAMBDA NIL (THOR2 T))
EXPR)

(DEFPROP THORT
 (LAMBDA NIL (THPOPT) THVALUE)
EXPR)

(DEFPROP THPOPT
 (LAMBDA NIL (SETQ THTREE (CDR THTREE)))
EXPR)

(DEFPROP THPROG
 (LAMBDA (THA) (THBIND (CAR THA)) (THPUSH THTREE (LIST (QUOTE THPROG) THA NIL THA)) (THPROGA))
FEXPR)

(DEFPROP THPROG
 THPROGT
THSUCCEED)

(DEFPROP THPROG
 THPROGF
THFAIL)

(DEFPROP THPROGA
 (LAMBDA NIL
  ((LAMBDA(X)
    (COND ((NULL (CDAR X)) (THPOPT) (QUOTE THNOVAL))
	  ((ATOM (CADAR X)) (SETQ THEXP (LIST (QUOTE THTAG) (CADAR X))) (RPLACA X (CDAR X)) THVALUE)
	  (T (SETQ THEXP (CADAR X)) (RPLACA X (CDAR X)) THVALUE)))
   (CDAR THTREE)))
EXPR)

(DEFPROP THPROGF
 (LAMBDA NIL (THBRANCHUN) NIL)
EXPR)

(DEFPROP THPROGT
 (LAMBDA NIL (THBRANCH) (THPROGA))
EXPR)

(DEFPROP THPURE
 (LAMBDA (XX) (ERRSET (MAPC (FUNCTION (LAMBDA (Y) (AND# (THVAR Y) (ERR NIL)))) XX)))
EXPR)

(DEFPROP THPUTPROP
 (LAMBDA(ATO VAL IND)
  (THPUSH THTREE
	  (LIST	(QUOTE THMUNG)
		(LIST
		 (LIST (QUOTE PUTPROP)
		       (LIST (QUOTE QUOTE) ATO)
		       (LIST (QUOTE QUOTE) (GET ATO IND))
		       (LIST (QUOTE QUOTE) IND)))))
  (PUTPROP ATO VAL IND))
EXPR)

(DEFPROP THREM1
 (LAMBDA(THB)
  (PROG	(THA THSV THA1 THA2 THA3 THA4 THA5 THONE THPC)
	(SETQ THNF (ADD1 THNF))
	(COND ((AND# (ATOM THB) (NOT (EQ THB (QUOTE ?))) (NOT (NUMBERP THB))) (SETQ THA THB))
	      ((OR# (EQ THB (QUOTE ?)) (MEMQ# (CAR THB) (QUOTE (THV THNV))))
	       (COND (THFST (RETURN (QUOTE THVRB))) ((SETQ THA (QUOTE THVRB)))))
	      (T (RETURN (QUOTE THVRB))))
	(SETQ THA1 (GET THA THWH))
	(COND (THA1) (T (RETURN NIL)))
	(COND ((EQ THA1 (QUOTE THNOHASH)) (RETURN (QUOTE THBQF))))
	(SETQ THA2 (THBA THNF THA1))
	(COND (THA2) (T (RETURN NIL)))
	(SETQ THA3 (THBA THAL (CADR THA2)))
	(COND (THA3) (T (RETURN NIL)))
	(SETQ THA4 (CADR THA3))
	(SETQ THPC (NOT (EQ THWH (QUOTE THASSERTION))))
	(SETQ THA5
	      (COND ((OR# THFST THFSTP) (THBAP THBS (CDR THA4)))
		    ((THBA (COND (THPC THON) (T (CAR THON))) (CDR THA4)))))
	(COND (THA5) (T (RETURN NIL)))
	(SETQ THONE (CADR THA5))
	(RPLACD THA5 (CDDR THA5))
	(COND
	 ((AND# (NOT (EQ (CADR THA4) 1)) (OR# (SETQ THSV (CDDR THA4)) T) (RPLACA (CDR THA4) (SUB1 (CADR THA4))))
	  (RETURN THONE)))
	(SETQ THSV (CDDR THA3))
	(RPLACD THA3 THSV)
	(COND ((CDADR THA2)) (T (RETURN THONE)))
	(SETQ THSV (CDDR THA2))
	(RPLACD THA2 THSV)
	(COND ((CDR THA1)) (T (RETURN THONE)))
	(REMPROP THA THWH)
	(RETURN THONE)))
EXPR)

(DEFPROP THREMBINDF
 (LAMBDA NIL (SETQ THALIST (CADAR THTREE)) (THPOPT) NIL)
EXPR)

(DEFPROP THREMBINDT
 (LAMBDA NIL (SETQ THALIST (CADAR THTREE)) (THPOPT) THVALUE)
EXPR)

(DEFPROP THREMOVE
 (LAMBDA(THB)
  (PROG	(THB1 THWH THNF THAL THON THBS THFST THFSTP THFOO)
	(SETQ THNF 0)
	(SETQ THB1
	      (COND ((ATOM THB) (SETQ THBS THB)
				(SETQ THWH (CAR (SETQ THB1 (GET THB (QUOTE THEOREM)))))
				(CADDR THB1))
		    ((SETQ THWH (QUOTE THASSERTION)) (SETQ THBS THB))))
	(SETQ THAL (LENGTH THB1))
	(SETQ THFST T)
   THP1	(COND ((NULL THB1) (SETQ THB1 THFOO)
			   (SETQ THNF 0)
			   (SETQ THFST (SETQ THFOO NIL))
			   (SETQ THFSTP T)
			   (GO THP1))
	      ((NULL (SETQ THON (THREM1 (CAR THB1)))) (RETURN NIL))
	      ((MEMQ# THON (QUOTE (THBQF THVRB)))
	       (SETQ THFOO (NCONC THFOO (LIST (COND ((EQ THON (QUOTE THVRB)) (CAR THB1))))))
	       (SETQ THB1 (CDR THB1))
	       (GO THP1)))
	(SETQ THFST NIL)
	(MAPC (FUNCTION THREM1) (CDR THB1))
	(SETQ THNF 0)
	(MAPC (FUNCTION THREM1) THFOO)
	(RETURN THON)))
EXPR)

(DEFPROP THREMPROP
 (LAMBDA(ATO IND)
  (THPUSH THTREE
	  (LIST	(QUOTE THMUNG)
		(LIST
		 (LIST (QUOTE PUTPROP)
		       (LIST (QUOTE QUOTE) ATO)
		       (LIST (QUOTE QUOTE) (GET ATO IND))
		       (LIST (QUOTE QUOTE) IND)))))
  (REMPROP ATO IND))
EXPR)

(DEFPROP THRESTRICT
 (LAMBDA(THB)
  (PROG	(X)
	(COND ((ATOM (SETQ X (THGAL (CAR THB) THALIST))) (THPRINTC (QUOTE THRESTRICT/ IGNORED/ -/ CONTINUING)))
	      ((THRPLACD (CDR X) (THUNION (CDDR X) (CDR THB)))))
	(RETURN X)))
FEXPR)

(DEFPROP THRETURN
 (LAMBDA (X) (APPLY# (QUOTE THSUCCEED) (CONS (QUOTE THPROG) X)))
FEXPR)

(DEFPROP THRPLACA
 (LAMBDA (X Y) (PROG (THML) (THRPLACAS X Y) (THPUSH THTREE (LIST (QUOTE THMUNG) THML)) (RETURN X)))
EXPR)

(DEFPROP THRPLACAS
 (LAMBDA (X Y) (THPUSH THML (LIST (QUOTE THURPLACA) X (CAR X))) (RPLACA X Y))
EXPR)

(DEFPROP THURPLACA
 (LAMBDA (L) (RPLACA (CAR L) (CADR L)))
FEXPR)

(DEFPROP THRPLACD
 (LAMBDA (X Y) (PROG (THML) (THRPLACDS X Y) (THPUSH THTREE (LIST (QUOTE THMUNG) THML)) (RETURN X)))
EXPR)

(DEFPROP THRPLACDS
 (LAMBDA (X Y) (THPUSH THML (LIST (QUOTE THURPLACD) X (CDR X))) (RPLACD X Y))
EXPR)

(DEFPROP THURPLACD
 (LAMBDA (L) (RPLACD (CAR L) (CADR L)))
FEXPR)

(DEFPROP THSETQ
 (LAMBDA(THL1)
  (PROG	(THML THL)
	(SETQ THL THL1)
   LOOP	(COND ((NULL THL) (THPUSH THTREE (LIST (QUOTE THMUNG) THML)) (RETURN THVALUE))
	      ((NULL (CDR THL)) (PRINT THL1) (THERT ODD NUMBER OF GOODIES - THSETQ))
	      ((ATOM (CAR THL))
	       (THPUSH THML (LIST (QUOTE SETQ) (CAR THL) (LIST (QUOTE QUOTE) (EVAL (CAR THL)))))
	       (SET (CAR THL) (SETQ THVALUE (EVAL (CADR THL)))))
	      (T (THRPLACAS (CDR (THSGAL (CAR THL))) (SETQ THVALUE (THVAL (CADR THL) THALIST)))))
	(SETQ THL (CDDR THL))
	(GO LOOP)))
FEXPR)

(DEFPROP THSGAL
 (LAMBDA(X)
  (OR# (ASSOC (CADR X) THALIST)
       (PROG (Y)
	     (SETQ Y (LIST (CADR X) (QUOTE THUNASSIGNED)))
	     (NCONC (GET (QUOTE THALIST) (QUOTE VALUE)) (LIST Y))
	     (RETURN Y))))
EXPR)

(DEFPROP THSTATE
 (LAMBDA(THINDICATORS)
  (PROG	(THP THSLIST THGRIN)
	(MAPC
	 (FUNCTION
	  (LAMBDA(BUCKET)
	   (MAPC
	    (FUNCTION
	     (LAMBDA(THATOM)
	      (MAPC
	       (FUNCTION
		(LAMBDA(THWH)
		 (AND#
		  (SETQ THP (GET THATOM THWH))
		  (SETQ THP (ASSOC 1 (CDR THP)))
		  (MAPC
		   (FUNCTION
		    (LAMBDA(LENGTH-BUCKET)
		     (MAPC
		      (FUNCTION
		       (LAMBDA(ASRT)
			(COND ((EQ THWH (QUOTE THASSERTION)) (SETQ THSLIST (CONS ASRT THSLIST)))
			      (T (SETQ THSLIST (CONS (NCONS ASRT) THSLIST)) (SETQ THGRIN (CONS ASRT THGRIN))))))
		      (CDDR LENGTH-BUCKET))))
		   (CDR THP)))))
	       (COND (THINDICATORS) ((QUOTE (THASSERTION THANTE THCONSE THERASING)))))))
	    BUCKET)))
	 OBLIST)
	(EVAL (CONS (QUOTE GRINDEF) (DREVERSE THGRIN)))
	(PRINT (QUOTE (THDATA)))
	(MAPC (FUNCTION PRINT) THSLIST)
	(PRINT NIL)))
FEXPR)

(DEFPROP THSUCCEED
 (LAMBDA(THA)
  (OR# (NOT THA)
       (PROG (THX)
	     (AND# (EQ (CAR THA) (QUOTE THEOREM)) (SETQ THA (CONS (QUOTE THPROG) (CDR THA))))
	     (SETQ THBRANCH THTREE)
	     (SETQ THABRANCH THALIST)
	LOOP (COND ((NULL THTREE) (PRINT THA) (THERT OVERPOP - THSUCCEED))
		   ((EQ (CAAR THTREE) (QUOTE THREMBIND)) (SETQ THALIST (CADAR THTREE)) (THPOPT) (GO LOOP))
		   ((EQ (CAAR THTREE) (CAR THA))
		    (THPOPT)
		    (RETURN (COND ((CDR THA) (EVAL (CADR THA))) ((QUOTE THNOVAL)))))
		   ((AND# (EQ (CAR THA) (QUOTE THTAG))
			  (EQ (CAAR THTREE) (QUOTE THPROG))
			  (SETQ THX (MEMQ# (CADR THA) (CADDDR (CAR THTREE)))))
		    (RPLACA (CDAR THTREE) (CONS NIL THX))
		    (RETURN (THPROGT)))
		   (T (THPOPT) (GO LOOP))))))
FEXPR)

(DEFPROP THTAE
 (LAMBDA(XX)
  (COND	((ATOM XX) NIL)
	((EQ (CAR XX) (QUOTE THUSE))
	 (MAPCAR (FUNCTION
		  (LAMBDA(X)
		   (COND ((NOT (AND# (SETQ THXX (GET X (QUOTE THEOREM))) (EQ (CAR THXX) TYPE)))
			  (PRINT X)
			  (LIST (QUOTE THAPPLY) (THERT BAD THEOREM -THTAE) (CAR THX)))
			 (T (LIST (QUOTE THAPPLY) X (CAR THX))))))
		 (CDR XX)))
	((EQ (CAR XX) (QUOTE THTBF))
	 (MAPCAN (FUNCTION (LAMBDA (Y) (COND (((CADR XX) Y) (LIST (LIST (QUOTE THAPPLY) Y (CAR THX)))))))
		 (COND (THY1 THY) ((SETQ THY1 T) (SETQ THY (THMATCHLIST (CAR THX) TYPE))))))
	(T (PRINT XX) (THTAE (THERT UNCLEAR RECCOMMENDATION -THTAE)))))
EXPR)

(DEFPROP THTAG
 (LAMBDA (L) (AND# (CAR L) (THPUSH THTREE (LIST (QUOTE THTAG) (CAR L)))))
FEXPR)

(DEFPROP THTAG
 THTAGT
THSUCCEED)

(DEFPROP THTAG
 THTAGF
THFAIL)

(DEFPROP THTAGF
 (LAMBDA NIL (THPOPT) NIL)
EXPR)

(DEFPROP THTAGT
 (LAMBDA NIL (THPOPT) THVALUE)
EXPR)

(DEFPROP THTRUE
 (LAMBDA (X) T)
EXPR)

(DEFPROP THTRY1
 (LAMBDA NIL
  (PROG	(THX THY THZ THW THEOREM)
	(SETQ THZ (CAR THTREE))
	(SETQ THY (CDDR THZ))
	(RPLACD THY (SUB1 (CDR THY)))
   NXTREC
	(COND ((OR# (NULL (CAR THY)) (ZEROP (CDR THY))) (RETURN NIL)))
	(SETQ THX (CAAR THY))
	(GO (CAR THX))
   THNUM
	(RPLACD THY (CADR THX))
	(RPLACA THY (CDAR THY))
	(GO NXTREC)
   THDBF
	(SETQ THOLIST THALIST)
	(COND ((NULL (CADDR THX)) (RPLACA THY (CDAR THY)) (GO NXTREC))
	      ((PROG (XVAL)
		     (SETQ XVAL (AND# ((CADR THX) (SETQ THW (CAADDR THX))) (THMATCH1 (CADR THZ) (CAR THW))))
		     (RPLACA (CDDR THX) (CDADDR THX))
		     (RETURN XVAL))
	       (RETURN THW))
	      (T (GO THDBF)))
   THTBF
	(COND ((NULL (CADDR THX)) (RPLACA THY (CDAR THY)) (GO NXTREC)))
	(SETQ THEOREM (CAADDR THX))
   THTBF1
	(COND
	 ((NOT (AND# (SETQ THW (GET THEOREM (QUOTE THEOREM))) (EQ (CAR THW) (QUOTE THCONSE))))
	  (PRINT THEOREM)
	  (COND ((EQ (SETQ THEOREM (THERT BAD THEOREM - THTRY1)) (QUOTE T)) (GO NXTREC)) (T (GO THTBF1)))))
	(COND ((PROG (XVAL)
		     (SETQ XVAL (AND# ((CADR THX) (CAADDR THX)) (THAPPLY1 THEOREM THW (CADR THZ))))
		     (RPLACA (CDDR THX) (CDADDR THX))
		     (RETURN XVAL))
	       (RETURN T))
	      (T (GO THTBF)))))
EXPR)

(DEFPROP THTRY
 (LAMBDA(X)
  (COND	((ATOM X) NIL)
	((EQ (CAR X) (QUOTE THTBF))
	 (COND ((NOT THZ1) (SETQ THZ1 T) (SETQ THZ (THMATCHLIST THA2 (QUOTE THCONSE)))))
	 (COND (THZ (LIST (LIST (QUOTE THTBF) (CADR X) THZ))) (T NIL)))
	((EQ (CAR X) (QUOTE THDBF))
	 (COND ((NOT THY1) (SETQ THY1 T) (SETQ THY (THMATCHLIST THA2 (QUOTE THASSERTION)))))
	 (COND (THY (LIST (LIST (QUOTE THDBF) (CADR X) THY))) (T NIL)))
	((EQ (CAR X) (QUOTE THUSE)) (LIST (LIST (QUOTE THTBF) (QUOTE THTRUE) (CDR X))))
	((EQ (CAR X) (QUOTE THNUM)) (LIST X))
	(T (PRINT X) (THTRY (THERT UNCLEAR RECOMMENDATION - THTRY)))))
EXPR)

(DEFPROP THUNDOF
 (LAMBDA NIL
  (COND	((NULL (CADDAR THTREE)) (THPOPT))
	(T (SETQ THXX (CDDAR THTREE))
	   (SETQ THALIST (CAADR THXX))
	   (RPLACA (CDR THXX) (CDADR THXX))
	   (SETQ THTREE (CAAR THXX))
	   (RPLACA THXX (CDAR THXX))))
  NIL)
EXPR)

(DEFPROP THUNDOT
 (LAMBDA NIL (THPOPT) T)
EXPR)

(DEFPROP THUNIQUE
 (LAMBDA(THA)
  (SETQ THA (CONS (QUOTE THUNIQUE) (MAPCAR (FUNCTION THUCI) THA)))
  (PROG	(X)
	(SETQ X THALIST)
   LP	(COND ((NULL X) (THPUSH THALIST THA) (RETURN T))
	      ((EQ (CAAR X) (QUOTE THUNIQUE)) (COND ((EQUAL (CAR X) THA) (RETURN NIL)))))
	(SETQ X (CDR X))
	(GO LP)))
FEXPR)

(DEFPROP THUCI
 (LAMBDA(A)
  (COND ((MEMQ (CAR A) (QUOTE (THV THNV))) (COND ((ATOM (SETQ A (THGAL A THALIST)))) ((CADR A)))) ((EVAL A))))
EXPR)

(DEFPROP THV1
 (LAMBDA(X)
  (SETQ THXX X)
  (COND	((EQ (SETQ X (CADR (OR# (ASSOC X THALIST) (PROG2 (PRINT THXX) (THERT THUNBOUND - THV1)))))
	     (QUOTE THUNASSIGNED))
	 (PRINT THXX)
	 (THERT THUNASSIGNED - THV1))
	(T X)))
EXPR)

(DEFPROP THV
 (LAMBDA (X) (THV1 (CAR X)))
FEXPR)

(DEFPROP THVAL
 (LAMBDA(THEXP THALIST)
  (THPUSH THLEVEL (LIST THTREE THALIST))
  (PROG	(THTREE THVALUE THBRANCH THOLIST THABRANCH THE THMESSAGE)
	(SETQ THV (QUOTE (THV THNV)))
	(SETQ THVALUE (QUOTE THNOVAL))
   GO	(SETQ THE THEXP)
	(SETQ THEXP NIL)
	(COND (↑A (SETQ ↑A NIL) (COND ((THERT ↑A - THVAL)) (T (GO FAIL)))))
	(AND (ATOM (ERRSET (SETQ THVALUE (EVAL THE)))) (ERR NIL))
   GO1	(COND (THMESSAGE (GO MFAIL)) (THEXP (GO GO)) (THVALUE (GO SUCCEED)) (T (GO FAIL)))
   SUCCEED
	(COND ((NULL THBRANCH) (SETQ THBRANCH THTREE) (SETQ THABRANCH THALIST)))
	(COND ((NULL THTREE) (SETQ THLEVEL (CDR THLEVEL)) (RETURN THVALUE))
	      ((SETQ THEXP (GET (CAAR THTREE) (QUOTE THSUCCEED))) (GO GO2))
	      ((THERT BAD SUCCEED - THVAL) (GO SUCCEED))
	      (T (GO FAIL)))
   MFAIL
	(COND ((EQ (CAR THMESSAGE) THTREE) (SETQ THEXP (CADR THMESSAGE)) (SETQ THMESSAGE NIL) (GO GO)))
   FAIL	(COND ((NULL THTREE) (SETQ THLEVEL (CDR THLEVEL)) (RETURN NIL))
	      ((SETQ THEXP (GET (CAAR THTREE) (QUOTE THFAIL))) (GO GO2))
	      ((THERT BAD FAIL - THVAL) (GO SUCCEED))
	      (T (GO FAIL)))
   GO2	(SETQ THVALUE ((PROG1 THEXP (SETQ THEXP NIL))))
	(GO GO1)))
EXPR)

(DEFPROP THVAR
 (LAMBDA (X) (MEMQ# (CAR X) (QUOTE (THV THNV))))
EXPR)

(DEFPROP THVARS2
 (LAMBDA(X)
  (PROG	(A)
	(COND ((ATOM X) (RETURN X)))
	(AND# (EQ (CAR X) (QUOTE THEV)) (SETQ X (THVAL (CADR X) THALIST)))
	(COND ((THVAR X)) (T (RETURN X)))
	(SETQ A (THGAL X THALIST))
	(RETURN
	 (COND ((EQ (CADR A) (QUOTE THUNASSIGNED)) X)
	       ((AND# THY (EQ (CAR X) (QUOTE THNV))) (THRPLACA (CDR A) (QUOTE THUNASSIGNED)) X)
	       (T (CADR A))))))
EXPR)

(DEFPROP THVARSUBST
 (LAMBDA(THX THY)
  (COND ((EQ (CAR THX) (QUOTE THEV)) (SETQ THX (THVAL (CADR THX) THALIST))) ((THVAR THX) (SETQ THX (EVAL THX))))
  (COND ((ATOM THX) THX) (T (MAPCAR (FUNCTION THVARS2) THX))))
EXPR)

(DEFPROP THVSETQ
 (LAMBDA(THA)
  (PROG	(A)
	(SETQ A THA)
   LOOP	(COND ((NULL A) (RETURN THVALUE))
	      ((NULL (CDR A)) (PRINT THA) (THERT ODD NUMBER OF GOODIES-THSETQ))
	      (T (SETQ THVALUE (CAR (RPLACA (CDR (THSGAL (CAR A))) (THVAL (CADR A) THALIST))))))
	(SETQ A (CDDR A))
	(GO LOOP)))
FEXPR)

(DEFPROP THMUNG
 THMUNGT
THSUCCEED)

(DEFPROP THMUNG
 THMUNGF
THFAIL)

(DEFPROP THUNDO
 THUNDOT
THSUCCEED)

(DEFPROP THUNDO
 THUNDOF
THFAIL)

(DEFPROP THREMBIND
 THREMBINDT
THSUCCEED)

(DEFPROP THREMBIND
 THREMBINDF
THFAIL)

(PUTPROP (QUOTE THSPRINT) (GET (QUOTE SPRINT) (QUOTE SUBR)) (QUOTE SUBR))

(DEFPROP SPRINT
 (LAMBDA(LST N)
  (PROG	(MSAV MSAV2)
	(SETQ MSAV (MODCHR 44 (MODCHR 101 NIL)))
	(SETQ MSAV2 (MODCHR 47 (MODCHR 101 NIL)))
	(THSPRINT (COND (THUNREADFLG (THUNREADM LST)) (T LST)) N)
	(MODCHR 44 MSAV)
	(MODCHR 47 MSAV2)))
EXPR)

(DEFPROP THUNREADM
 (LAMBDA(EXP)
  (PROG	(CHAR)
	(RETURN
	 (COND ((SETQ CHAR (ASSOC# EXP THUNREAD1)) (CDR CHAR))
	       ((ATOM EXP) EXP)
	       ((AND (CDR EXP) (NULL (CDDR EXP)) (ATOM (CADR EXP)) (SETQ CHAR (ASSOC (CAR EXP) THUNREAD2)))
		(MAKNAM (APPEND (CDR CHAR) (EXPLODE (CADR EXP)))))
	       (T (CONS (THUNREADM (CAR EXP)) (THUNREADM (CDR EXP))))))))
EXPR)

(DEFPROP THREAD
 (LAMBDA NIL
  (PROG	(CHAR X)
	(RETURN
	 (SELECTQ (SETQ CHAR (READCH))
		  (? (LIST (QUOTE THV) (READ)))
		  (: (LIST (QUOTE THV) (READ)))
		  (E (LIST (QUOTE THEV) (READ)))
		  (← (LIST (QUOTE THNV) (READ)))
		  (& (PROG NIL CHLP (COND ((NEQ (QUOTE &) (READCH)) (GO CHLP)))))
		  (T (QUOTE (THTBF THTRUE)))
		  (R (QUOTE THRESTRICT))
		  (G (QUOTE THGOAL))
		  (A (QUOTE THASSERT))
		  (P (QUOTE $P))
		  (N (LIST (QUOTE THANUM) (READ)))
		  (COND	((SETQ X (ASSOC THUSERCHARS)) (EVAL (CONS (QUOTE PROGN) (CDR X))))
			((PRINT (QUOTE ILLEGAL-PREFIX))
			 (PRINC (QUOTE $))
			 (PRINC CHAR)
			 (PRINC (READ))
			 (ERR NIL)))))))
EXPR)

(DEFPROP THUSERCHARS
 (THUSERCHARS)
VALUE)

(DEFPROP THERT
 (LAMBDA(/0ERTA)
  (PROG	(/0LISTEN ↑W ↑Q /0RETVAL /0RETFLAG)
	(SETQ ↑Q (INC NIL NIL))
	(SETQ ↑W (OUTC NIL NIL))
	(SETQ /0LEVEL (ADD1 /0LEVEL))
	(PRINT (QUOTE >>>))
	(COND ((EQ (CAR /0ERTA) (QUOTE TH%0%)) (MAPC (FUNCTION THPRINT2) (CDR /0ERTA)) (INC ↑Q (SETQ ↑Q NIL)))
	      (/0ERTA (MAPC (FUNCTION THPRINT2) /0ERTA)
		      (PRINT (QUOTE LISTENING))
		      (OR# THLEVEL (THPRINT2 (QUOTE THVAL)))))
	(SETQ /0RETVAL T)
   /0LISTEN
	(SETQ THINF NIL)
	(SETQ /0RETFLAG NIL)
	(TERPRI)
	(PRINC /0LEVEL)
	(COND
	 ((AND (OR (CONSP
		    (ERRSET
		     (COND ((EQ (SETQ /0LISTEN (READ)) (QUOTE $P)) (SETQ /0RETFLAG T))
			   ((AND# (NOT (ATOM /0LISTEN)) (EQ (CAR /0LISTEN) (QUOTE $P)))
			    (SETQ /0RETVAL (EVAL (CADR /0LISTEN)))
			    (SETQ /0RETFLAG T))
			   (THLEVEL (PRINT (EVAL /0LISTEN)))
			   (T (PRINT (THVAL /0LISTEN THALIST))))))
		   THLEVEL)
	       (NULL /0RETFLAG))
	  (GO /0LISTEN)))
	(SETQ /0LEVEL (SUB1 /0LEVEL))
	(INC ↑Q NIL)
	(OUTC ↑W NIL)
	(RETURN /0RETVAL)))
FEXPR)

(DEFPROP THEDIT
 (LAMBDA(X)
  (PROG	(Y)
	(COND ((NULL X) (SETQ X (NCONS LASTWORD))))
	(COND ((SETQ Y (GET (CAR X) (QUOTE THEOREM)))
	       (EDITE Y (CDR X) (CAR X))
	       (RETURN (SETQ LASTWORD (CAR X))))
	      (T (PRINT (CAR X)) (PRINC (QUOTE IS/ NOT/ EDITABLE)) (ERR NIL)))))
FEXPR)

(DEFPROP THINIT
 (LAMBDA NIL
  (SETQ THINF (SETQ THTREE (SETQ THLEVEL NIL)))
  (SETQ /0LEVEL -1)
  (COND
   (THUSERMESSAGES (MAPC (FUNCTION (LAMBDA (X) (TERPRI) (PRINC X))) THUSERMESSAGES)
		   (SETQ THUSERMESSAGES NIL)
		   (AND (ERRSET (INC (INPUT DSK: (INIT . PLN)) NIL) NIL) (THERT TH%0% READING (INIT . PLN)))))
  (AND THUSERINITFN (THUSERINITFN))
  (TERPRI)
  (THERT TOP LEVEL))
EXPR)

(DEFPROP THTRACE
 (LAMBDA (L) (MAPC (FUNCTION THTRACE1) L) L)
FEXPR)

(DEFPROP THTRACE
 (THTRACE)
VALUE)

(DEFPROP THTRACE1
 (LAMBDA(X)
  (PROG	(Y)
	(SETQ X
	      (COND ((ATOM X) (LIST X T NIL))
		    ((CDDR X) X)
		    ((NULL (CDR X)) (PRINT X) (PRINC (QUOTE BAD/ FORMAT)) (RETURN NIL))
		    ((LIST (CAR X) (CADR X) NIL))))
	(COND
	 ((GET (CAR X) (QUOTE THEOREM))
	  (COND	((SETQ Y (ASSOC (QUOTE THEOREM) THTRACE))
		 (RPLACD Y (QUOTE ((THSEL (QUOTE CADR)) (THSEL (QUOTE CADDR))))))
		((SETQ THTRACE
		       (LIST X
			     (APPEND (QUOTE (THEOREM (THSEL (QUOTE CADR)) (THSEL (QUOTE CADDR)))) THTRACE)))))))
	(COND ((SETQ Y (ASSOC (CAR X) THTRACE)) (RPLACD Y (CDR X))) ((SETQ THTRACE (CONS X THTRACE))))
	(RETURN X)))
EXPR)

(DEFPROP THUNTRACE
 (LAMBDA(L)
  (COND	(L
	 (SETQ THTRACE
	       (MAPCAN (FUNCTION (LAMBDA (X) (COND ((MEMQ# (CAR X) L) (PRINT X) NIL) ((LIST X))))) THTRACE)))
	(THTRACE (MAPC (FUNCTION PRINT) THTRACE) (SETQ THTRACE NIL)))
  (QUOTE DONE))
FEXPR)

(DEFPROP THTRACES
 (LAMBDA(THF THL)
  (PROG	(THY THZ THB)
	(AND# (SETQ THY (ASSOC THF THTRACE))
	      (OR# (SETQ THB (THVAL (CADDR THY) THALIST)) (THVAL (CADR THY) THALIST))
	      (OR# (SETQ THZ (GET THF (QUOTE THTRACE))) (THERT THTRACES - TRACE LOSSAG))
	      (THZ THL THB)
	      THB
	      (THERT))))
EXPR)

(DEFPROP THTRACES
 (LAMBDA NIL (PRINT (CADAR THTREE)) (PRINC (QUOTE SUCCEEDED/ )) (EVLIS (CDDAR THTREE)) (THPOPT) THVALUE)
THSUCCEED)

(DEFPROP THTRACES
 (LAMBDA NIL (PRINT (CADAR THTREE)) (PRINC (QUOTE FAILED/ )) (EVLIS (CDDAR THTREE)) (THPOPT) NIL)
THFAIL)

(DEFPROP THSEL
 (LAMBDA(THF)
  (PROG (THX) (RETURN (AND# (SETQ THX (ASSOC THL THTRACE)) (SETQ THX (THF THX)) (THVAL THX THALIST)))))
EXPR)

(DEFPROP THGENS
 (LAMBDA (X) (MAKNAM (NCONC (EXPLODE (CAR X)) (EXPLODE (SETQ THGENS (ADD1 THGENS))))))
FEXPR)

(DEFPROP THGENS
 (THGENS . 0)
VALUE)

(DEFPROP THEOREM
 (LAMBDA(X B)
  (THPUSH THTREE (LIST (QUOTE THTRACES) X (QUOTE (AND# THVALUE (PRIN1 THVALUE))) (AND# B (QUOTE (THERT)))))
  (THPRINTC (QUOTE ENTERING/ THEOREM))
  (PRIN1 X))
THTRACE)

(DEFPROP THUNREADFLG
 (THUNREADFLG)
VALUE)

(DEFPROP THUNREAD1
 (THUNREAD1 ((THTBF THTRUE) . $T) (THRESTRICT . $R) (THGOAL . $G) (THASSERT . $A))
VALUE)

(DEFPROP THUNREAD2
 (THUNREAD2 (THV $ ?) (THNV $ ←) (THANUM $ N) (QUOTE '))
VALUE)

(DEFPROP GRINPROPS
 (NIL EXPR FEXPR MACRO VALUE SPECIAL THEOREM THSUCCEED THFAIL THTRACE)
VALUE)

(DEFPROP THUSERINITFN
 (THUSERINITFN)
VALUE)

(DEFPROP ↑A
 (↑A)
VALUE)

(DEFPROP THXX
 (THXX)
VALUE)

(DEFPROP THALIST
 (THALIST (NIL NIL))
VALUE)

(DEFPROP THUSERMESSAGES
 (THUSERMESSAGES MICRO-PLANNER)
VALUE)

(DEFPROP PLNRINITFN
 (LAMBDA (X) (PROG1 THUSERINITFN (SETQ THUSERINITFN X)))
EXPR)

(PROGN
 (DEFPROP PINIT
	  (LAMBDA NIL
	   (PROG (X)
		 (RPLACD (MEMQ# (QUOTE THEOREM) GRINPROPS) NIL)
		 (MODCHR (CHRVAL (QUOTE ')) (MODCHR (CHRVAL (QUOTE /@)) NIL))
		 (DRM $ THREAD)
		 (DRM : THREAD)
		 (INITFN (QUOTE THINIT))
		 (EXCISE)
		 (SETQ KLIST NIL)
		 (PUTPROP (QUOTE INITFN) (CADR (SETQ X (GETL (QUOTE PLNRINITFN) (QUOTE (EXPR SUBR))))) (CAR X))
		 (SETQ THUNREADFLG T)
		 (REMOB PLNRFNS PINIT PLNRINITFN)))
	  EXPR))